
open HolKernel boolLib bossLib Parse ppc_Lib; val _ = new_theory "ppc_tests";


(* add 1,2,3 *)
val _ = ppc_test "7C221A14"
  [("PC","A0000000"),("GPR1","4444"),("GPR2","2222"),("GPR3","3333"),("CTR","123AA"),
   ("A0000000","7C"),("A0000001","22"),("A0000002","1A"),("A0000003","14"),("A0000FFF","88"),("CARRY","T")]
  [("PC","A0000004"),("GPR1","5555"),("GPR2","2222"),("GPR3","3333"),("CTR","123AA"),
   ("A0000000","7C"),("A0000001","22"),("A0000002","1A"),("A0000003","14"),("A0000FFF","88"),("CARRY","T")]

(* subfic 19, 26, -2 *)
val _ = ppc_test "227AFFFE"
  [("PC","A0344560"),("GPR26","11"),("GPR19","222"),("LR","FFFF"),
   ("A0344560","22"),("A0344561","7A"),("A0344562","FF"),("A0344563","FE"),("A0000FFF","88"),("CARRY","T")]
  [("PC","A0344564"),("GPR26","11"),("GPR19","FFFFFFED"),("LR","FFFF"),
   ("A0344560","22"),("A0344561","7A"),("A0344562","FF"),("A0344563","FE"),("A0000FFF","88"),("CARRY","T")]

(* sthx 2, 26, 4 *)
val _ = ppc_test "7C5A232E"
  [("PC","A0344560"),("GPR26","4000A0"),("GPR2","AABBCCDD"),("GPR4","8"),
   ("A0344560","7C"),("A0344561","5A"),("A0344562","23"),("A0344563","2E"),("CARRY","T"),
   ("4000A8","00"),("4000A9","00")]
  [("PC","A0344564"),("GPR26","4000A0"),("GPR2","AABBCCDD"),("GPR4","8"),
   ("A0344560","7C"),("A0344561","5A"),("A0344562","23"),("A0344563","2E"),("CARRY","T"),
   ("4000A8","CC"),("4000A9","DD")]

(* lwz 19, 234(26) *)
val _ = ppc_test "827A00EA"
  [("PC","A0344560"),("GPR26","400006"),("GPR19","8"),
   ("A0344560","82"),("A0344561","7A"),("A0344562","00"),("A0344563","EA"),("CR02","T"),
   ("4000F0","11"),("4000F1","22"),("4000F2","33"),("4000F3","44")]
  [("PC","A0344564"),("GPR26","400006"),("GPR19","11223344"),
   ("A0344560","82"),("A0344561","7A"),("A0344562","00"),("A0344563","EA"),("CR02","T"),
   ("4000F0","11"),("4000F1","22"),("4000F2","33"),("4000F3","44")]


val _ = export_theory ();
